Nuprl Lemma : member_wf
9,38
postcript
pdf
A
:Type,
a
:
A
. (
a
A
)
Type
latex
ProofTree
Definitions
t
T
,
x
:
A
.
B
(
x
)
origin
A:Type, a:A. (a 
A) Type
A:Type, a:A. (a A) Type
Tx:A. B(x)